package ewu

import scala.collection.mutable.ArrayBuffer
import java.util.ArrayList
import lang.LOC
import ewu._
import gui._
import scala.swing._
import scala.swing.Dialog._

/**
 * Eine Anweisungsfolge enthält beliebig viele Objekte des Typs "Anweisung". Die Nummerierung
 * der einzelnen Anweisungen erfolgt hier zentral. Die dafür in der Klasse definierte
 * "numerate" ruft für jede Anweisung deren originäre Methode auf. Analog wird die
 * propagate-Methode ausgeführt. Hier erfolgt allerdings keine Ausgabe; dafür ist die 
 * protocol-Methode zuständig, die auch den noch händisch auszuführenden Beweisbedarf anzeigt.
 * Mehrere Hilfsmethoden à la addAnweisung() ermöglichen eine vereinfachte Nutzung im Sinne
 * des Refactorings.
 */

case class Anweisungsfolge (var anweisungsfolge: ArrayBuffer[Anweisung]) {

  def addAnweisung(wert: Anweisung, pos: Int) = {
    var tmp: ArrayBuffer[Anweisung] = ArrayBuffer()
    var tmpPos: Int = 1

    if(pos == 0)
      tmp.append(wert)
    for(i <- anweisungsfolge) {
      if(tmpPos != pos)
        tmp.append(i)
      else {
        tmp.append(i)
        tmp.append(wert)
      }
      tmpPos += 1
    }
    this.anweisungsfolge = tmp
  }
  
  def addAnweisung(wert: Anweisung) = {
    anweisungsfolge.append(wert)
  }
  
  def addAnweisungen(wert: Anweisungsfolge) = {
    for(i <- wert.anweisungsfolge)
      anweisungsfolge.append(i)
  }

  def joinAnweisung(tmpAnweisungsfolge: Anweisungsfolge, pos: Int) = {
    var tmp: ArrayBuffer[Anweisung] = ArrayBuffer()
    var tmpPos: Int = 1

    for(i <- anweisungsfolge) {
      if(tmpPos == pos) {
        for(j <- tmpAnweisungsfolge.anweisungsfolge)
          tmp.append(j)
      }
      else
        tmp.append(i)
      tmpPos += 1
    }

    this.anweisungsfolge = tmp
  }

  def getLaenge(): Int = {
    return anweisungsfolge.length
  }

  def getNum(elm: Anweisung): Int = {
    return anweisungsfolge.indexOf(elm)+1
  }

  def getElem(num: Int): Anweisung = {
    if((num-1) < anweisungsfolge.size && (num-1) >= 0)
      return anweisungsfolge(num-1)
    else
      return null
  }

  def numerate(num: List[Int]) = {
    var tmpNum: List[Int] = num
    for(i <- anweisungsfolge) {
      i match {
        case Assertion(prefix: String, expr: BoolExpression) =>
          null
        case x:Bound =>
          null
        case _ =>
          i.numerate(tmpNum)
          tmpNum = (tmpNum.head+1) :: tmpNum.tail
      }
    }
  }
  
  def tabbate(i: Int) = {
    for(j <- anweisungsfolge)
      j.tabbate(i)
  }
  
  def traceB(): Boolean = {
    var tmp: Bound = null;
      for(j <- anweisungsfolge) {
        j match {
          case Bound (prefix: String, expr: Expression) =>
            tmp = Bound (prefix, expr)
          case Schleife (bedingung: BoolExpression, doTeil: Anweisungsfolge) =>
            if(tmp != null) {
              j.setBound(tmp)
              tmp = null
            }
            doTeil.traceB
          case _ =>
            null
        }
      }
      return true
  }
  
  def trace(h: Int, umgebung: Environment, tt: Layout): (String, Boolean, Int) = {
    var ausgabe: String = ""
    var r: Result.Value = null
    var Th = h

    ausgabe ++= umgebung.toString ++ "\n"
    for(i <- anweisungsfolge) {
      i match {
        case Bound (prefix: String, expr: Expression) =>
          Th += 1
          
        case Assertion (prefix: String, expr: BoolExpression) =>
          var (tmpAusgabe, cont, count) = i.trace(umgebung, null, tt, Th)
          Th = count
          ausgabe ++= tmpAusgabe //++ umgebung.toString ++ "\n"
          
          if(!cont) {
            var r: Result.Value = null
            r = Dialog.showConfirmation(tt, LOC.get("AuswertungFalse")+ "\n" + tmpAusgabe,
                                        LOC.get("Fehler"), Dialog.Options.YesNo,
                                        Dialog.Message.Question)
            if(r.equals(Result.No)) {
              return (ausgabe, false, Th)
            }
          }

        case _ =>
          var (tmpAusgabe, cont, count) = i.trace(umgebung, null, tt, Th)
          Th = count
          ausgabe ++= tmpAusgabe ++ umgebung.toString ++ "\n"
          if(!cont) return (ausgabe, false, Th)
      }

      if(Th >= Layout.tracesteps) {
        r = Dialog.showConfirmation(tt, LOC.get("TraceLimit"), LOC.get("TraceLimitTitel"),
                                    Dialog.Options.YesNo, Dialog.Message.Question)
        if(r.equals(Result.No)) {
          return (ausgabe, false, 0)
        }
        else
          Th = 0
      }
    }
    
    return (ausgabe, true, Th)
  }

  override def toString(): String = {
    var ausgabe: String = ""
    for(i <- anweisungsfolge)
      ausgabe ++= i.toString
    return ausgabe
  }
  
  def toTabString(): String = {
    var ausgabe: String = ""
    for(i <- anweisungsfolge)
      ausgabe ++= i.toTabString
    return ausgabe
  }

  def propagate = {
    for(i <- anweisungsfolge) {
      i match {
        case _: Schleife =>
          var zv = this.getElem(this.getNum(i)-1)
          if(zv != null && zv.isInstanceOf[Assertion])
            this.joinAnweisung(i.propagate(zv), this.getNum(i))
        case _: Fall =>
          var zv = this.getElem(this.getNum(i)-1)
          var zn = this.getElem(this.getNum(i)+1)
          if(zv != null && zn != null && zv.isInstanceOf[Assertion]
                  && zn.isInstanceOf[Assertion])
            this.joinAnweisung(i.propagate(zv, zn), this.getNum(i))
        case _ =>
          null
      }
    }

    for(i <- anweisungsfolge.reverse) {
      i match {
        case _: Zuweisung =>
          var zn = this.getElem(this.getNum(i)+1)
          if(zn != null) {
            if(zn.isInstanceOf[Bound])
              zn = this.getElem(this.getNum(i)+2)
            if(zn.isInstanceOf[Assertion])
              this.joinAnweisung(i.propagate(zn), this.getNum(i))
          }
        case _ =>
          null
      }
    }
  }

  def protocol(): String = {
    var ausgabe: String = ""
    var tmp: Anweisung = null

    for(i <- anweisungsfolge) {
      i match {
        case Assertion (prefix: String, expr: BoolExpression) =>
          if(tmp != null) {
            ausgabe ++= LOC.get("Kosequenzregel") ++ "\n" ++ LOC.get("Separator") ++ "\n"
            ausgabe ++= tmp.toString ++ "=>\n" ++ i.toString ++ "\n"
            tmp = null
          }
          else {
            tmp = i

          }
        case Schleife (bedingung: BoolExpression, doTeil: Anweisungsfolge) =>
          tmp = null
          ausgabe ++= doTeil.protocol
        case Fall (bedingung: BoolExpression, thenTeil: Anweisungsfolge,
                          elseTeil: Anweisungsfolge) =>
          tmp = null
          ausgabe ++= thenTeil.protocol
          ausgabe ++= elseTeil.protocol
        case _ =>
          tmp = null
      }
    }

    return ausgabe
  }
  
  def toCheckVersion(addfuncs: ArrayList[String], arrayvars: ArrayList[String]) : Anweisungsfolge = {
    var ret = new Anweisungsfolge(new ArrayBuffer())
    var actfall = ret
    
    for(i <- anweisungsfolge) {
      i match {
        case x:Assertion => 
          var cv = x.toCheckVersion(addfuncs, arrayvars)

          actfall.addAnweisung(cv._1)
          actfall = cv._2;
        case x:Schleife =>
          var ne = x.copy(x.bedingung, x.doTeil.toCheckVersion(addfuncs, arrayvars))
          actfall.addAnweisung(ne)
        case x:Fall =>
          var ne = x.copy(x.bedingung, x.thenTeil.toCheckVersion(addfuncs, arrayvars), x.elseTeil.toCheckVersion(addfuncs, arrayvars))
          actfall.addAnweisung(ne)
        case x => actfall.addAnweisung(x)
      }
    }
    return ret
  }
  
  def getVariables() : ArrayBuffer[Name] = {
    var ret:ArrayBuffer[Name] = new ArrayBuffer()
    for(i <- 0 to anweisungsfolge.length-1) {
      anweisungsfolge(i).getVariables(ret)
    }
    return ret
  }
  
  def replaceVariable(fromVar: Name, toVar: Expression) : Unit = {
    for(i <- 0 to anweisungsfolge.length-1) {
      anweisungsfolge(i).replaceVariable(fromVar, toVar)
    }
  }
  
}


 